COMMENT ⊗   VALID 00010 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	representations of functions: two approaches
C00003 00003	first approach: functions as association lists
C00006 00004	facts about alists
C00009 00005	second approach: functions as lists of numbers
C00011 00006	* alist induction
C00013 00007	proof of facts about alists
C00016 00008	samemap
C00017 00009	apparently stronger definition of samemap
C00023 00010	extensionality
C00027 ENDMK
C⊗;
;representations of functions: two approaches
(wipe-out)
(get-proofs nth)
;first approach: functions as association lists

(proof appalist)

(decl dom (type: |GROUND→GROUND|))
(defax dom |∀xa y alist.dom nil=nil∧
                        dom((xa.y).alist)=xa.dom alist| )
(label domdef)

(decl range (type: |GROUND→GROUND|))
(defax range |∀xa y alist.range nil=nil∧
                          range((xa.y).alist)=y.range alist| )
(label rangedef)

(decl functp (type: |GROUND→TRUTHVAL|))
(define functp |∀alist.functp(alist)≡uniqueness dom(alist)|)
(label functdef)

(decl injectp (type: |GROUND→TRUTHVAL|))
(define injectp |∀alist.injectp(alist)≡functp(alist)∧uniqueness range(alist)|)
(label injectdef)

(decl (appalist) (type: |ground⊗ground→ground|))
(define appalist |∀alist y.appalist(y,alist)=cdr assoc(y,alist)|)
(label appalistdef)

(decl (samemap) (type: |ground⊗ground→truthval|))
(define samemap 
 |∀alist alist1.samemap(alist,alist1)≡
                mklset dom(alist)=mklset dom(alist1)∧
                (∀y.yεmklset dom(alist)⊃appalist(y,alist)=appalist(y,alist1))|)
(label samemapdef)

(define permutp |∀alist.permutp(alist)≡
                        functp(alist)∧mklset(dom(alist))=mklset(range(alist))|)
(label permutp_def)

(axiom |∀chi.chi(nil)∧(∀xa y alist.chi(alist)⊃chi((xa.y).alist))⊃(∀alist.chi(alist))|)
(label alistinduction)

;facts about alists

(proof alistfacts)

(axiom |∀alist.listp(dom alist)|)
(label domsort)(label simpinfo)

(axiom |∀alist.listp(range alist)|)
(label rangesort)(label simpinfo)

(axiom |∀alist.length (dom(alist))=length alist|)
(label domlength)

(axiom |∀alist.length(dom(alist))=length(range(alist))|)
(label domrangelength)

(axiom |∀alist y.sexp appalist(y,alist)|)
(label appalistsort)(label simpinfo)

(axiom |∀alist y.¬yεmklset(dom(alist))⊃appalist(y,alist)=nil|)
(label trivial_appalist)

;Exercise:
;∀alist z.member(z,range alist)⊃(∃x.member(x.z,alist))
;(label member_range)

;∀alist x z.member(x.z,alist)⊃member(z,range(alist))
;(label membership_alist_range)

;∀alist x z.x=appalist(z,alist)∧atom assoc(z,alist)⊃null x
;(label trivial_assoc)

(axiom |∀alist.samemap(alist,alist)|)
(label samemap_equivalence)

(axiom |∀alist alist1.samemap(alist,alist1)⊃samemap(alist1,alist)|)
(label samemap_equivalence)

(axiom 
   |∀alist alist1 alist2.
       samemap(alist,alist1)∧samemap(alist1,alist2)⊃samemap(alist,alist2)|)
(label samemap_equivalence)

(axiom |∀alist1 alist2.samemap(alist1,alist2)≡
                       (mklset(dom(alist1))=mklset(dom(alist2))∧
                       (∀x.appalist(x,alist1)=appalist(x,alist2)))|)
(label samemap_def1)
;second approach: functions as lists of numbers

(proof appl)

(define appl |∀u i.appl(u,i)=nth(u,i)|)
(label appldef)

;extensionality for functions 

(axiom |∀u v.length u=length v∧(∀i.i<length u⊃appl(u,i)=appl(v,i))⊃u=v|)
(label extensionality)
 
(axiom |∀u i.i<length u ⊃ sexp(appl(u,i))∧member(appl(u,i),u)|)
(label applfacts) (label simpinfo)

;predicates for functions 

(decl (into) (type: |ground→truthval|))
(define into |∀u.into(u)=(∀n.n<length u⊃natnum nth(u,n)∧nth(u,n)<length u)|)
(label intodef)

(decl (onto) (type: |ground→truthval|))
(define onto |∀u.onto(u)=(into(u)∧(∀n.n<length u⊃member(n,u)))|)
(label ontodef)
 
(decl (perm) (type: |ground→truthval|))
(define perm |∀u.perm(u)=onto(u)|)

;injectivity is given by the predicate inj

(save-proofs appl)
;* alist induction

(wipe-out)
(get-proofs appal)
(proof alistind)

(assume |chi nil|)
(label alind0)

(assume |∀xa y alist.chi(alist)⊃chi((xa.y).alist)|)
(label alind1)

(assume |alistp u⊃chi u|)
(label alind2)

(assume |alistp (x.u)|)
(label alind3)

(ue (alist |x.u|) alistdef *)
;¬ATOM X∧ATOM CAR X∧ALISTP U

(ue ((xa.|car x|)(y.|cdr(x)|)(alist.u)) alind1 * alind3 alind2)
;CHI(X.U)
;deps: (ALIND1 ALIND2 ALIND3)

(ci alind3)
;ALISTP X.U⊃CHI(X.U)
;deps: (ALIND1 ALIND2)

(ci alind2)
;(ALISTP U⊃CHI(U))⊃(ALISTP X.U⊃CHI(X.U))
;deps: (ALIND1)

(ue (phi |λu.alistp(u)⊃chi(u)|) listinduction * alind0 alind1)
;∀U.ALISTP U⊃CHI(U)

(derive |∀alist.chi alist| *)
;deps: (ALIND0 ALIND1)

(ci (alind0 alind1))
;CHI(NIL)∧(∀XA Y ALIST.CHI(ALIST)⊃CHI((XA.Y).ALIST))⊃(∀ALIST.CHI(ALIST))
;proof of facts about alists

(wipe-out)
(get-proofs appal)
(proof alistproofs)

(unlabel simpinfo domsort rangesort appalistsort)
;domsort

(ue (chi |λalist.listp dom(alist)|) alistinduction (open dom))
;∀ALIST.LISTP DOM(ALIST)
(label simpinfo domsort)

;rangesort

(ue (chi |λalist.listp range(alist)|) alistinduction (open range))
;∀ALIST.LISTP RANGE(ALIST)
(label simpinfo rangesort)

;domlength

(ue (chi |λalist.length dom alist=length alist|) alistinduction (open dom))
;∀ALIST.LENGTH (DOM(ALIST))=LENGTH ALIST

;domrangelength 

(ue (chi |λalist.length(dom alist)=length(range alist)|) alistinduction 
    (open dom range))
;∀ALIST.LENGTH (DOM(ALIST))=LENGTH (RANGE(ALIST))

;appalistsort

(ue (chi |λalist.sexp appalist(y,alist)|) alistinduction 
    (part 1(open appalist assoc)))
;∀ALIST.SEXP APPALIST(Y,ALIST)
(label simpinfo appalistsort)

;trivial appalist

(ue (chi |λalist.¬(yεmklset dom(alist))⊃appalist(y,alist)=nil|) alistinduction
    (part 1 (open epsilon mklset dom appalist assoc member)))
;∀ALIST.¬YεMKLSET(DOM(ALIST))⊃APPALIST(Y,ALIST)=NIL

;member range

(ue (chi |λalist.member(z,range alist)⊃(∃x.member(x.z,alist))|)
    alistinduction 
    (open range member)(use normal mode: always))
;∀ALIST.MEMBER(Z,RANGE(ALIST))⊃(∃X.MEMBER(X.Z,ALIST))

;membership alist range

(trw |∀x y.x=y⊃cdr x=cdr y|)
;∀X Y.X=Y⊃CDR X=CDR Y

(ue ((x.|x.z|)(y.|xa.y|)) *)
;X.Z=XA.Y⊃Z=Y

(ue (chi |λalist.member(x.z,alist)⊃member(z,range alist)|)
    alistinduction
    (open appalist assoc range member)
    (use demorgan1 * normal mode: always))
;∀ALIST.MEMBER(X.Z,ALIST)⊃MEMBER(Z,RANGE(ALIST))

;trivial assoc

;(ue (chi |λalist.x=cdr assoc(z,alist)∧atom assoc(z,alist)⊃null x|) alistinduction
;    (open assoc))
;∀ALIST.X=CDR ASSOC(Z,ALIST)∧ATOM ASSOC(Z,ALIST)⊃NULL X
;samemap

(trw |samemap(alist,alist)|(open samemap))
;SAMEMAP(ALIST,ALIST)

(trw |samemap(alist,alist1)⊃samemap(alist1,alist)| (open samemap mklset dom))
;SAMEMAP(ALIST,ALIST1)⊃SAMEMAP(ALIST1,ALIST)

(trw |samemap(alist,alist1)∧samemap(alist1,alist2)⊃samemap(alist,alist2)|
    (open samemap mklset dom))
;SAMEMAP(ALIST,ALIST1)∧SAMEMAP(ALIST1,ALIST2)⊃SAMEMAP(ALIST,ALIST2)

;apparently stronger definition of samemap

(wipe-out)
(get-proofs appl)
(proof samemap)

(assume |samemap(alist1,alist2)|)

(rw * (open samemap))
;MKLSET(DOM(ALIST1))=MKLSET(DOM(ALIST2))∧
;(∀Y.YεMKLSET(DOM(ALIST1))⊃APPALIST(Y,ALIST1)=APPALIST(Y,ALIST2))

(trw |¬yεmklset(dom(alist1))⊃appalist(y,alist1)=appalist(y,alist2)|
     (use trivial_appalist mode: always) 
     (use * mode: exact))
;¬YεMKLSET(DOM(ALIST1))⊃APPALIST(Y,ALIST1)=APPALIST(Y,ALIST2)

(ue ((q.|yεmklset dom(alist1)|)(p.|appalist(y,alist1)=appalist(y,alist2)|))
    excluded_middle * -2)
;APPALIST(Y,ALIST1)=APPALIST(Y,ALIST2)

(derive |mklset(dom(alist1))=mklset(dom(alist2))∧
         ∀y.appalist(y,alist1)=appalist(y,alist2)| (-3 *))

(ci -5)
;SAMEMAP(ALIST1,ALIST2)⊃
;MKLSET(DOM(ALIST1))=MKLSET(DOM(ALIST2))∧
;(∀Y.APPALIST(Y,ALIST1)=APPALIST(Y,ALIST2))

(derive |samemap(alist1,alist2)≡
	(mklset(dom(alist1))=mklset(dom(alist2))∧
	(∀x.appalist(x,alist1)=appalist(x,alist2)))| *)

;extensionality
(wipe-out)
(get-proofs appl)

(proof extensionality)

(assume |length u=length v|)
(label ext1)

(assume |N<LENGTH U|)
(label ext2)

(assume |(∀I.I<LENGTH (NTHCDR(U,N'))⊃NTH(NTHCDR(U,N'),I)=NTH(NTHCDR(V,N'),I))⊃
         NTHCDR(U,N')=NTHCDR(V,N')|) (label ext_indhyp)

(assume |(∀I.I<LENGTH (NTHCDR(U,N'))'⊃
          NTH(NTH(U,N).NTHCDR(U,N'),I)=NTH(NTHCDR(V,N),I))|)(label ext3)

(rw ext2 (use ext1 mode: exact))
;N<LENGTH V
(label ext4)

(rw ext3 (use ext4 mode: exact)
    (use nthcdr_car_cdr ue: ((u.v)(n.n)) ext4 mode: exact))
(label ext5)
;∀I.I<LENGTH (NTHCDR(U,N'))'⊃
;   NTH(NTH(U,N).NTHCDR(U,N'),I)=NTH(NTH(V,N).NTHCDR(V,N'),I)


(ue (i |0|) * (open nth))
;NTH(U,N)=NTH(V,N)
(label ext6)

(ue (i |i'|) ext5 (open nth))
;I<LENGTH (NTHCDR(U,N'))⊃NTH(NTHCDR(U,N'),I)=NTH(NTHCDR(V,N'),I)

(derive |nthcdr(u,n')=nthcdr(v,n')| (ext_indhyp *))
 
(trw |nth(u,n).nthcdr(u,n')=nthcdr(v,n)| 
 (use nthcdr_car_cdr ue: ((u.v)(n.n)) ext4 mode: exact) (use ext6 * mode: exact))
;NTH(U,N).NTHCDR(U,N')=NTHCDR(V,N)
;deps: (EXT1 EXT2 EXT_INDHYP EXT3)

(ci ext3)
;(∀I.I<LENGTH (NTHCDR(U,N'))'⊃NTH(NTH(U,N).NTHCDR(U,N'),I)=NTH(NTHCDR(V,N),I))⊃
;NTH(U,N).NTHCDR(U,N')=NTHCDR(V,N)

(ci ext_indhyp)

(ci ext2)
;N<LENGTH U⊃
;(((∀I.I<LENGTH (NTHCDR(U,N'))⊃NTH(NTHCDR(U,N'),I)=NTH(NTHCDR(V,N'),I))⊃
;  NTHCDR(U,N')=NTHCDR(V,N'))⊃
; ((∀I.I<LENGTH (NTHCDR(U,N'))'⊃
;      NTH(NTH(U,N).NTHCDR(U,N'),I)=NTH(NTHCDR(V,N),I))⊃
;  NTH(U,N).NTHCDR(U,N')=NTHCDR(V,N)))
;deps: (EXT1)

(trw |nthcdr(v,length u)| (use ext1 last_nthcdr mode: exact))
;NTHCDR(V,LENGTH U)=NIL

(ue  ((phi4.|λu n.(∀i.i<length u⊃appl(u,i)=appl(nthcdr(v,n),i))⊃u=nthcdr(v,n)|)
      (u.u)) nthcdr_induction1 (open appl) * -2)
;(∀I.I<LENGTH U⊃NTH(U,I)=NTH(V,I))⊃U=V

(ci ext1)
;LENGTH U=LENGTH V⊃((∀I.I<LENGTH U⊃NTH(U,I)=NTH(V,I))⊃U=V)

(derive |∀u v.length u=length v∧(∀i.i<length u⊃appl(u,i)=appl(v,i))⊃u=v| *)

;applfact has been proved already for nth

(trw |∀u i.i<length u ⊃ sexp(appl(u,i))∧member(appl(u,i),u)| (open appl) nthmember)
;∀U I.I<LENGTH U⊃SEXP APPL(U,I)∧MEMBER(APPL(U,I),U)